i, x:Id, a:Knd, T, A:Type, f:(ATA).
@i: ma-single-effect0(x;A;a;T;f)  Dsys
& (D:Dsys.
& (@i: ma-single-effect0(x;A;a;T;f)  D
& ( D 
& ( realizes es.
& ( vartype(i;x)  A & (e:E. loc(e) = i  Id  kind(e) = a  Knd  valtype(e)  T)
& ( & (e:E.
& ( & (loc(e) = i  Id  kind(e) = a  Knd  (x after e) = f((x when e),val(e))  A)) 

latex

Definitions

Void, x:A. B(x), Top, KindDeq, x:A. B(x), P  Q, {T}, SQType(T), s = t, Prop, s ~ t, left+right, x:AB(x), loc(e), valtype(e), E, Dsys, b, D1  D2, World, FairFifo, IdDeq, <a,b>, A & B, P & Q, x:AB(x), s.x, x when e, Valtype(da;k), PossibleWorld(D;w), vartype(i;x), D realizes es. P(es), f(x)?z, State(ds), x. t(x), ma-single-effect0(x;A;k;T;f), ES(the_w), kind(e), f(a), x.A(x), x : v, Type, Knd, a:A fp B(a), t  T, Id

Lemmas

fpf-single wf, s-effect-rule, fpf-cap wf, top wf, ma-state wf, dsys wf, d-sub wf, world wf, fair-fifo wf, possible-world wf, id-deq wf, es-E wf, es-kind wf, Id wf, es-loc wf, w-es wf, Knd sq, fpf-cap-single1, Knd wf, Kind-deq wf